i:Id, k:Knd. has-src(i;k)   

latex

Definitions	false, t  T, IdLnk, Id, x.A(x), x:A. B(x), x. t(x), 1of(t), source(l), a = b, lnk(k), isrcv(k), has-src(i;k), left+right, Knd,
Lemmas	Knd wf, eq id wf, lsrc wf, pi1 wf, Id wf, IdLnk wf, bfalse wf